 $LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
 require 'ext_pr1_v4'

class Object
#Shape1d ::= Range1d | Union1d

def shape1d?()
 self.range1d? or self== Union1d
end

#Shape2d ::= Range2d | Union2d

def shape2d?()
  self== Range2d or self== Union2d
end

#UnionShape ::= Union1d | Union2d

def union_shape?()
  self== Union1d or self== Union2d
end

#GraphObj ::= Point | Shape

def graph_obj?()
  self.point? or self.shape?
end

#Point ::= Point1d | Point2d

def point?()
  self .point1d? or self== Point2d
end

#Shape ::= PrimShape | CompShape

def shape?()
  self.prim_shape? or self.comp_shape?
end

#CompShape ::= UnionShape

def comp_shape?()
  self.union_shape?
end

#PrimShape ::= Range1d | Range2d

def prim_shape?()
    self.range1d? or self== Range2d
end
end
 #Fehlerbehebung weil er die find_min und find_max Methoden sonst nicht findet
class Integer
  def find_min(r2) self < r2 ? self : r2 end
  def find_max(r2) self < r2 ? r2 : self end
end
 #
#Datendefinitionen:
#
#1D Objekte
#
#Point1d ::= Int
 
class Point1d

 def initialize(int) 
   @int = int
 end
 
  def invariant?() 
    @int.int?
  end

  def int()
    @int
  end
  
  def point1d?
    self == Point1d
  end
  
  def ==(value)
    value == Point1d
#    puts(value)
#     if (value .point1d?) then
#        value.int == @int
#     else 
#       false
#     end
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  if (self.shape1d? and point.point1d?) then
    self.trans1d(point)
  elsif (self.shape2d? and point== Point2d) then
    self.trans2d(point)
  elsif (self.point1d? and point.point1d?) then
    self.trans0d(point)
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point2)  
  Point1d[self.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(point1d)
  check_pre((self.shape1d? and point1d.point1d?))
  if (self.range1d?) then
    Range1d[(self.first).trans0d(point1d), (self.last).trans0d(point1d)]
  elsif self== Union1d then
    Union1d[(self.left).trans1d(point1d), (self.right).trans1d(point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(point2d)
  check_pre((self.shape2d? and point2d== Point2d))
  if (self== Range2d) then
    Range2d[(self.x_range).trans1d(point2d.x),(self.y_range).trans1d(point2d.y)]
  elsif self== Union2d then
    Union2d[(self.left).trans2d(point2d), (self.right).trans2d(point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
    if (self.range1d? and r2.range1d?) then
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (self== Range2d and r2== Range2d) then
      x_first = (self.x_range.first.int).find_min(r2.x_range.first.int)
      x_last = (self.x_range.last.int).find_max(r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = (self.y_range.first.int).find_min(r2.y_range.first.int)
      y_last = (self.y_range.last.int).find_max(r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end

#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  if (self.union_shape?) then
    if (not (self.left).union_shape? and not (self.right).union_shape?) then
      (self.left).bounding_range(self.right)
    else
      (self.left).bounds
      (self.right).bounds
    end
  else
    (self.left).bounding_range(self.right)
  end
end

#def find_min(r2) self < r2 ? self : r2 end
#
#def find_max(r2) self < r2 ? r2 : self end

#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#

def graph_equal_v1_?(o2)
  check_pre((self.graph_obj? and o2.graph_obj?))
  self.graph_equal_?(o2)
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o2)
   check_pre((self.graph_obj? and o2.graph_obj?))
   if (self .point1d? and o2 .point1d?) or
      (self== Point2d and o2== Point2d) or 
      (self.shape1d? and o2.shape1d?) or
      (self.shape2d? and o2.shape2d?) then
      self == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
  check_pre(((self.point? and o2.point?) or (self.shape? and o2.shape?)))
  # Punkte sind immer Deckungsgleich!!! IMMER!
  if (self.point1d? and o2.point1d?) or (self== Point2d and o2== Point2d) then
      self == o2
  elsif (self.shape1d? and o2.shape1d?) then
      if (self.range1d? and o2.range1d?) then
        ((self.last.int) - (self.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  elsif (self.shape2d? and o2.shape2d?) then
      if (self== Range2d and o2== Range2d) then
        ((self.x_range.first.int) - (self.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((self.y_range.first.int) - (self.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val2)
  check_pre((self.point? and val2.shape?))
 if (self.point1d? and val2.shape1d?) then
   self.int.between?(val2.first.int, val2.last.int)
 elsif (self== Point2d and val2.shape2d?) then
   (self.x.int < val2.x_range.first.int or 
    self.x.int > val2.x_range.last.int  or 
    self.y.int < val2.y_range.first.int  or 
    self.y.int > val2.y_range.last.int)
 elsif (self.point1d? and val2== Union1d) or (self== Point2d and val2== Union2d) then
   self.in?(val2)
 end
end

end

#Range1d ::= Range[first,last] :: Point1d x Point1d

class Range1d

  def initialize(first, last) 
   @first = first
   @last = last
  end
 
  def invariant?()
    @first .point1d? and @last .point1d?
  end
  
  def range1d?()
    self.first == Range1d or self.last  == Range1d
  end
  
  def first()
    @first
  end
  
  def last()
    @last
  end
  
  def ==(value)
     if (value == Range1d) then
        value.first() == @first
        value.last() == @last
     else 
       false
     end
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  if (self.shape1d? and point.point1d?) then
    self.trans1d(point)
  elsif (self.shape2d? and point== Point2d) then
    self.trans2d(point)
  elsif (self.point1d? and point.point1d?) then
    self.trans0d(point)
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point2)  
  Point1d[self.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(point1d)
  check_pre((self.shape1d? and point1d.point1d?))
  if (self.range1d?) then
    Range1d[(self.first).trans0d(point1d), (self.last).trans0d(point1d)]
  elsif self== Union1d then
    Union1d[(self.left).trans1d(point1d), (self.right).trans1d(point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(point2d)
  check_pre((self.shape2d? and point2d== Point2d))
  if (self== Range2d) then
    Range2d[(self.x_range).trans1d(point2d.x),(self.y_range).trans1d(point2d.y)]
  elsif self== Union2d then
    Union2d[(self.left).trans2d(point2d), (self.right).trans2d(point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
    if (self.range1d? and r2.range1d?) then
      puts(self)
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (self== Range2d and r2== Range2d) then
      x_first = (self.x_range.first.int).find_min(r2.x_range.first.int)
      x_last = (self.x_range.last.int).find_max(r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = (self.y_range.first.int).find_min(r2.y_range.first.int)
      y_last = (self.y_range.last.int).find_max(r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end

#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  if (self.union_shape?) then
    if (not (self.left).union_shape? and not (self.right).union_shape?) then
      (self.left).bounding_range(self.right)
    else
      (self.left).bounds
      (self.right).bounds
    end
  else
    (self.left).bounding_range(self.right)
  end
end

#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool

def graph_equal_v1_?(o2)
  check_pre((self.graph_obj? and o2.graph_obj?))
  self.graph_equal_?(o2)
end

#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o2)
   check_pre((self.graph_obj? and o2.graph_obj?))
   if (self.point1d? and o2.point1d?) or
      (self== Point2d and o2== Point2d) or 
      (self.shape1d? and o2.shape1d?) or
      (self.shape2d? and o2.shape2d?) then
      self == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
  check_pre(((self.point? and o2.point?) or (self.shape? and o2.shape?)))
  # Punkte sind immer Deckungsgleich!!! IMMER!
  if (self.point1d? and o2.point1d?) or (self== Point2d and o2== Point2d) then
       self == o2
  elsif (self.shape1d? and o2.shape1d?) then
      if (self.range1d? and o2.range1d?) then
        ((self.last.int) - (self.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  elsif (self.shape2d? and o2.shape2d?) then
      if (self== Range2d and o2== Range2d) then
        ((self.x_range.first.int) - (self.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((self.y_range.first.int) - (self.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val2)
  check_pre((self.point? and val2.shape?))
 if (self.point1d? and val2.shape1d?) then
   self.int.between?(val2.first.int, val2.last.int)
 elsif (self== Point2d and val2.shape2d?) then
   (self.x.int < val2.x_range.first.int or 
    self.x.int > val2.x_range.last.int  or 
    self.y.int < val2.y_range.first.int  or 
    self.y.int > val2.y_range.last.int)
 elsif (self.point1d? and val2== Union1d) or (self== Point2d and val2== Union2d) then
   self.in?(val2)
 end
end

end
#SINN?
#def range1d(o)
#  check_pre((o.first.point1d? and o.last.point1d?))
#  
#end

#Union1d ::= Union1d[left,right] :: Shape1d x Shape1d

class Union1d
  
  def initialize(left, right)
    @right = right
    @left = left
  end
  
  def invariant?()
    shape1d?()
  end
  
  def ==(value)
     if (value == Union1d) then
        value.right() == @right
        value.left() == @left
     else 
       false
     end
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  
   #Shape1d ::= Range1d | Union1d

def shape1d?()
 (self.left .range1d? or self.left == Union1d) and (self.right .range1d? or self.right == Union1d)
end

  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  if (self.shape1d? and point.point1d?) then
    self.trans1d(point)
  elsif (self.shape2d? and point== Point2d) then
    self.trans2d(point)
  elsif (self.point1d? and point.point1d?) then
    self.trans0d(point)
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point2)  
  Point1d[self.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(point1d)
  check_pre((self.shape1d? and point1d.point1d?))
  if (self.range1d?) then
    Range1d[(self.first).trans0d(point1d), (self.last).trans0d(point1d)]
  elsif self== Union1d then
    Union1d[(self.left).trans1d(point1d), (self.right).trans1d(point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(point2d)
  check_pre((self.shape2d? and point2d== Point2d))
  if (self== Range2d) then
    Range2d[(self.x_range).trans1d(point2d.x),(self.y_range).trans1d(point2d.y)]
  elsif self== Union2d then
    Union2d[(self.left).trans2d(point2d), (self.right).trans2d(point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
    if (self.range1d? and r2.range1d?) then
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (self== Range2d and r2== Range2d) then
      x_first = (self.x_range.first.int).find_min(r2.x_range.first.int)
      x_last = (self.x_range.last.int).find_max(r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = (self.y_range.first.int).find_min(r2.y_range.first.int)
      y_last = (self.y_range.last.int).find_max(r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end


#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  if (self.union_shape?) then
    if (not (self.left).union_shape? and not (self.right).union_shape?) then
      (self.left).bounding_range(self.right)
    else
      (self.left).bounds
      (self.right).bounds
    end
  else
    (self.left).bounding_range(self.right)
  end
end
#def find_min(r2) self < r2 ? self : r2 end
#
#def find_max(r2) self < r2 ? r2 : self end

#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#

def graph_equal_v1_?(o2)
  check_pre((self.graph_obj? and o2.graph_obj?))
  self.graph_equal_?(o2)
end
#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o2)
   check_pre((self.graph_obj? and o2.graph_obj?))
   if (self.point1d? and o2.point1d?) or
      (self== Point2d and o2== Point2d) or 
      (self.shape1d? and o2.shape1d?) or
      (self.shape2d? and o2.shape2d?) then
      self == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
  check_pre(((self.point? and o2.point?) or (self.shape? and o2.shape?)))
  # Punkte sind immer Deckungsgleich!!! IMMER!
  if (self.point1d? and o2.point1d?) or (self== Point2d and o2== Point2d) then
      self == o2
  elsif (self.shape1d? and o2.shape1d?) then
      if (self.range1d? and o2.range1d?) then
        ((self.last.int) - (self.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  elsif (self.shape2d? and o2.shape2d?) then
      if (self== Range2d and o2== Range2d) then
        ((self.x_range.first.int) - (self.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((self.y_range.first.int) - (self.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val2)
  check_pre((self.point? and val2.shape?))
 if (self.point1d? and val2.shape1d?) then
   self.int.between?(val2.first.int, val2.last.int)
 elsif (self== Point2d and val2.shape2d?) then
   (self.x.int < val2.x_range.first.int or 
    self.x.int > val2.x_range.last.int  or 
    self.y.int < val2.y_range.first.int  or 
    self.y.int > val2.y_range.last.int)
 elsif (self.point1d? and val2== Union1d) or (self== Point2d and val2== Union2d) then
   self.in?(val2)
 end
end

end

#2D Objekte
#
#Point2d :: = Point2d[x,y] :: Point1d x Point1d

class Point2d
 def initialize(x, y)
   @x = x
   @y = y
 end
  
 def invariant?()
   x .point1d?
   y .point1d?
 end
 
 def ==(value)
     if (value == Point2d) then
        value.x() == @x
        value.y() == @y
     else 
       false
     end
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  if (self.shape1d? and point.point1d?) then
    self.trans1d(point)
  elsif (self.shape2d? and point== Point2d) then
    self.trans2d(point)
  elsif (self.point1d? and point.point1d?) then
    self.trans0d(point)
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point2)  
  Point1d[self.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(point1d)
  check_pre((self.shape1d? and point1d.point1d?))
  if (self.range1d?) then
    Range1d[(self.first).trans0d(point1d), (self.last).trans0d(point1d)]
  elsif self== Union1d then
    Union1d[(self.left).trans1d(point1d), (self.right).trans1d(point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(point2d)
  check_pre((self.shape2d? and point2d== Point2d))
  if (self== Range2d) then
    Range2d[(self.x_range).trans1d(point2d.x),(self.y_range).trans1d(point2d.y)]
  elsif self== Union2d then
    Union2d[(self.left).trans2d(point2d), (self.right).trans2d(point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
    if (self.range1d? and r2.range1d?) then
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (self== Range2d and r2== Range2d) then
      x_first = (self.x_range.first.int).find_min(r2.x_range.first.int)
      x_last = (self.x_range.last.int).find_max(r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = (self.y_range.first.int).find_min(r2.y_range.first.int)
      y_last = (self.y_range.last.int).find_max(r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end


#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  if (self.union_shape?) then
    if (not (self.left).union_shape? and not (self.right).union_shape?) then
      (self.left).bounding_range(self.right)
    else
      (self.left).bounds
      (self.right).bounds
    end
  else
    (self.left).bounding_range(self.right)
  end
end
#def find_min(r2) self < r2 ? self : r2 end
#
#def find_max(r2) self < r2 ? r2 : self end

#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#

def graph_equal_v1_?(o2)
  check_pre((self.graph_obj? and o2.graph_obj?))
  self.graph_equal_?(o2)
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o2)
   check_pre((self.graph_obj? and o2.graph_obj?))
   if (self.point1d? and o2.point1d?) or
      (self== Point2d and o2== Point2d) or 
      (self.shape1d? and o2.shape1d?) or
      (self.shape2d? and o2.shape2d?) then
      self == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
  check_pre(((self.point? and o2.point?) or (self.shape? and o2.shape?)))
  # Punkte sind immer Deckungsgleich!!! IMMER!
  if (self.point1d? and o2.point1d?) or (self== Point2d and o2== Point2d) then
      self == o2
  elsif (self.shape1d? and o2.shape1d?) then
      if (self.range1d? and o2.range1d?) then
        ((self.last.int) - (self.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  elsif (self.shape2d? and o2.shape2d?) then
      if (self== Range2d and o2== Range2d) then
        ((self.x_range.first.int) - (self.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((self.y_range.first.int) - (self.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val2)
  check_pre((self.point? and val2.shape?))
 if (self.point1d? and val2.shape1d?) then
   self.int.between?(val2.first.int, val2.last.int)
 elsif (self== Point2d and val2.shape2d?) then
   (self.x.int < val2.x_range.first.int or 
    self.x.int > val2.x_range.last.int  or 
    self.y.int < val2.y_range.first.int  or 
    self.y.int > val2.y_range.last.int)
 elsif (self.point1d? and val2== Union1d) or (self== Point2d and val2== Union2d) then
   self.in?(val2)
 end
end

end

#Range2d ::= Range2d[x_range,y_range] :: (Range1d x Range1d)

class Range2d
 def initialize(x_range, y_range)
   @x_range = x_range
   @y_range = y_range
 end
  
 def invariant?()
   x_range .range1d?
   y_range .range1d?
 end
 
 def ==(value)
     if (value == Range2d) then
        value.x_range() == @x_range
        value.y_range() == @y_range
     else 
       false
     end
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  if (self.shape1d? and point.point1d?) then
    self.trans1d(point)
  elsif (self.shape2d? and point== Point2d) then
    self.trans2d(point)
  elsif (self.point1d? and point.point1d?) then
    self.trans0d(point)
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point2)  
  Point1d[self.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(point1d)
  check_pre((self.shape1d? and point1d.point1d?))
  if (self.range1d?) then
    Range1d[(self.first).trans0d(point1d), (self.last).trans0d(point1d)]
  elsif self== Union1d then
    Union1d[(self.left).trans1d(point1d), (self.right).trans1d(point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(point2d)
  check_pre((self.shape2d? and point2d== Point2d))
  if (self== Range2d) then
    Range2d[(self.x_range).trans1d(point2d.x),(self.y_range).trans1d(point2d.y)]
  elsif self== Union2d then
    Union2d[(self.left).trans2d(point2d), (self.right).trans2d(point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
    if (self.range1d? and r2.range1d?) then
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (self== Range2d and r2== Range2d) then
      x_first = (self.x_range.first.int).find_min(r2.x_range.first.int)
      x_last = (self.x_range.last.int).find_max(r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = (self.y_range.first.int).find_min(r2.y_range.first.int)
      y_last = (self.y_range.last.int).find_max(r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end


#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  if (self.union_shape?) then
    if (not (self.left).union_shape? and not (self.right).union_shape?) then
      (self.left).bounding_range(self.right)
    else
      (self.left).bounds
      (self.right).bounds
    end
  else
    (self.left).bounding_range(self.right)
  end
end

#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#

def graph_equal_v1_?(o2)
  check_pre((self.graph_obj? and o2.graph_obj?))
  self.graph_equal_?(o2)
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o2)
   check_pre((self.graph_obj? and o2.graph_obj?))
   if (self.point1d? and o2.point1d?) or
      (self== Point2d and o2== Point2d) or 
      (self.shape1d? and o2.shape1d?) or
      (self.shape2d? and o2.shape2d?) then
      self == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
  check_pre(((self.point? and o2.point?) or (self.shape? and o2.shape?)))
  # Punkte sind immer Deckungsgleich!!! IMMER!
  if (self.point1d? and o2.point1d?) or (self== Point2d and o2== Point2d) then
      self == o2
  elsif (self.shape1d? and o2.shape1d?) then
      if (self.range1d? and o2.range1d?) then
        ((self.last.int) - (self.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  elsif (self.shape2d? and o2.shape2d?) then
      if (self== Range2d and o2== Range2d) then
        ((self.x_range.first.int) - (self.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((self.y_range.first.int) - (self.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val2)
  check_pre((self.point? and val2.shape?))
 if (self.point1d? and val2.shape1d?) then
   self.int.between?(val2.first.int, val2.last.int)
 elsif (self== Point2d and val2.shape2d?) then
   (self.x.int < val2.x_range.first.int or 
    self.x.int > val2.x_range.last.int  or 
    self.y.int < val2.y_range.first.int  or 
    self.y.int > val2.y_range.last.int)
 elsif (self.point1d? and val2== Union1d) or (self== Point2d and val2== Union2d) then
   self.in?(val2)
 end
end

end

#Union2d ::= Union2d[left,right] :: Shape2d x Shape2d

class Union2d

 def initialize(left, right)
   @left = left
   @right = right
 end
  
 def invariant?()
   shape2d?()  
 end
 
 def ==(value)
     if (value == Union2d) then
        value.left() == @left
        value.right() == @right
     else 
       false
     end
  end
  
  def self.[](*args) check_inv(self.new(*args)) end
#Shape2d ::= Range2d | Union2d

def shape2d?()
  (self.left== Range2d or self.left== Union2d) and (self.right== Range2d or self.right== Union2d)
end

  #translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(point)
  if (self.shape1d? and point.point1d?) then
    self.trans1d(point)
  elsif (self.shape2d? and point== Point2d) then
    self.trans2d(point)
  elsif (self.point1d? and point.point1d?) then
    self.trans0d(point)
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point2)  
  Point1d[self.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(point1d)
  check_pre((self.shape1d? and point1d.point1d?))
  if (self.range1d?) then
    Range1d[(self.first).trans0d(point1d), (self.last).trans0d(point1d)]
  elsif self== Union1d then
    Union1d[(self.left).trans1d(point1d), (self.right).trans1d(point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(point2d)
  check_pre((self.shape2d? and point2d== Point2d))
  if (self== Range2d) then
    Range2d[(self.x_range).trans1d(point2d.x),(self.y_range).trans1d(point2d.y)]
  elsif self== Union2d then
    Union2d[(self.left).trans2d(point2d), (self.right).trans2d(point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r2)
    if (self.range1d? and r2.range1d?) then
      first = (self.first.int).find_min(r2.first.int)
      last = (self.last.int).find_max(r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (self== Range2d and r2== Range2d) then
      x_first = (self.x_range.first.int).find_min(r2.x_range.first.int)
      x_last = (self.x_range.last.int).find_max(r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = (self.y_range.first.int).find_min(r2.y_range.first.int)
      y_last = (self.y_range.last.int).find_max(r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end


#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds()
  if (self.union_shape?) then
    if (not (self.left).union_shape? and not (self.right).union_shape?) then
      (self.left).bounding_range(self.right)
    else
      (self.left).bounds
      (self.right).bounds
    end
  else
    (self.left).bounding_range(self.right)
  end
end
#def find_min(r2) self < r2 ? self : r2 end
#
#def find_max(r2) self < r2 ? r2 : self end

#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#

def graph_equal_v1_?(o2)
  check_pre((self.graph_obj? and o2.graph_obj?))
  self.graph_equal_?(o2)
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o2)
   check_pre((self.graph_obj? and o2.graph_obj?))
   if (self.point1d? and o2.point1d?) or
      (self== Point2d and o2== Point2d) or 
      (self.shape1d? and o2.shape1d?) or
      (self.shape2d? and o2.shape2d?) then
      self == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o2)
  check_pre(((self.point? and o2.point?) or (self.shape? and o2.shape?)))
  # Punkte sind immer Deckungsgleich!!! IMMER!
  if (self.point1d? and o2.point1d?) or (self== Point2d and o2== Point2d) then
      self == o2
  elsif (self.shape1d? and o2.shape1d?) then
      if (self.range1d? and o2.range1d?) then
        ((self.last.int) - (self.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  elsif (self.shape2d? and o2.shape2d?) then
      if (self== Range2d and o2== Range2d) then
        ((self.x_range.first.int) - (self.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((self.y_range.first.int) - (self.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        (self.bounds()).graph_equal_trans?(o2.bounds())
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val2)
  check_pre((self.point? and val2.shape?))
 if (self.point1d? and val2.shape1d?) then
   self.int.between?(val2.first.int, val2.last.int)
 elsif (self== Point2d and val2.shape2d?) then
   (self.x.int < val2.x_range.first.int or 
    self.x.int > val2.x_range.last.int  or 
    self.y.int < val2.y_range.first.int  or 
    self.y.int > val2.y_range.last.int)
 elsif (self.point1d? and val2== Union1d) or (self== Point2d and val2== Union2d) then
   self.in?(val2)
 end
end

end
